COMMENT ⊗ VALID 00003 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 know3.lsp[f81,jmc] ekl axioms for knowledge using possible worlds
C00011 00003 Here come the wisemen axioms in the new formalism.
C00013 ENDMK
C⊗;
;;; know3.lsp[f81,jmc] ekl axioms for knowledge using possible worlds
(proof know3ax)
(decl (w w0 w1 w2 w3) world)
(decl RW world constant)
(decl (s s0 s1 s2 s3) person)
(decl (t t0 t1 t2 t3) time)
(decl join |person⊗person*→person| functional nil nil nil both)
(decl a |world⊗world⊗person⊗time → truthval| constant)
(decl (p p0 p1 p2 p3 q q0 q1 q2 q3) proposition)
(decl (equiv1) |proposition⊗proposition → proposition| constant nil infix 830)
(decl (implies1) |proposition⊗proposition → proposition| constant nil infix 840)
(decl (and1) |proposition⊗proposition* → proposition| functional nil infix 860 both)
(decl (or1) |proposition⊗proposition* → proposition| functional nil infix 850 both)
(decl (not1) |proposition → proposition| constant nil unary 870)
(decl true1 |proposition⊗world → truthval| constant)
(decl (knows knowsw) |person⊗proposition⊗time → proposition| constant)
;;; We don't need much about times for most purposes. I suppose
;;; we won't need many facts about the successor relation for times.
;;; Maybe we should use an ordering instead.
(decl succ |(time → time) ∨ (person → person)| functional)
;;; Let's have an ordering of times and also an ordering of persons.
(decl < |(time⊗time→truthval) ∨ (person⊗person→truthval)| functional nil infix 840)
(decl ≤ |(time⊗time→truthval) ∨ (person⊗person→truthval)| functional nil infix 840)
;;; Less than or equal
(axiom |∀s1 s2.s1≤s2 ≡ s1<s2 ∨ s1=s2|)
(axiom |∀t1 t2.t1≤t2 ≡ t1<t2 ∨ t1=t2|)
;;; We have to relate succession and inequality.
(axiom |∀t.t < succ(t)|)
;;; definitions of imitation propositional operators
(axiom |∀p q w.true1(p and1 q,w) ≡ true1(p,w) ∧ true1(q,w)|)
(axiom |∀p q w.true1(p or1 q,w) ≡ true1(p,w) ∨ true1(q,w)|)
(axiom |∀p q w.true1(p implies1 q,w) ≡ true1(p,w) ⊃ true1(q,w)|)
(axiom |∀p w.true1(not1 p,w) ≡ ¬true1(p,w)|)
(axiom |∀p q w.true1(p equiv1 q,w) ≡ (true1(p,w) ≡ true1(q,w))|)
;;; Reflexivity of accessibility distinguishes knowledge from belief. It
;;; asserts that what one knows is true.
;;; Maybe we'll weaken this eventually. Taking Boolos seriously would
;;; suggest it.
(axiom |∀w s t.a(w,w,s,t)|)
;;; Transitivity of accessibility amounts to knowing what one knows.
;;; It gives S4 in modal logic. It won't always be used.
;;; We'll leave it here for now, but I suspect we'll omit it in order
;;; to avoid the Montague paradoxes. We can leave it, because we
;;; don't have to use it in any particular proof.
(axiom |∀w1 w2 w3 s t.a(w1,w2,s,t) ∧ a(w2,w3,s,t) ⊃ a(w1,w3,s,t)|)
;;; Together with the previous two axioms, this symmetry makes accessibility an
;;; equivalence relation. This corresponds to S5 in modal logic. It
;;; means that when one doesn't know a proposition, one knows that one
;;; doesn't know it. Again most proofs won't use it.
(axiom |∀w1 w2 s t.a(w1,w2,s,t) ⊃ a(w2,w1,s,t)|)
;;; The fundamental definition of knowledge using accessibility.
(axiom |∀w s p.true1(knows(s,p,t),w) ≡ ∀w1.a(w,w1,s,t) ⊃ true1(p,w)|)
;;; Knowledge persists, i.e. no forgetting.
(axiom |∀w1 w2 s t1 t2.t1 < t2 ∧ a(w1,w2,s,t2) ⊃ a(w1,w2,s,t1)|)
;;; s1 < s2 says that whatever s1 knows, s2 knows that s1 knows it.
;;; In our system this relation is time independent.
(axiom |∀s1 s2 w1 w2 w3 t.s1<s2 ∧ a(w1,w2,s2,t) ∧ a(w2,w3,s1,t) ⊃ a(w1,w3,s1,t)|)
;;; The successor of a time is obvious enough. The successor of a person
;;; is a new and fancy concept. It is what the person would be if he
;;; jumped to the conclusion that what he knew was true. It will get us
;;; out of the Montague paradoxes, we hope. We may eventually want to
;;; make the successor of a person time dependent. Thus he has to express
;;; confidence in himself in order to become his own successor.
;;; Perhaps we shall come to prefer a system in which a person comes
;;; to express confidence only in some part of his knowledge that he
;;; has "written down".
(axiom |∀s.s < succ(s)|)
(axiom |∀s1 s2.join(s1,s2) ≤ s1 ≤ join(s1,s2) ≤ s2|)
(axiom |∀s1 s2.join(s1,s2) = join(s2,s1)|)
(axiom |∀s p t.knowsw(s,p,t) = knows(s,p,t) or1 knows(s,not1 p,t)|)
(decl (learns learnsw) |person⊗proposition⊗time→proposition| constant)
(axiom |∀w s p t.true1(learns(s,p,t),w)
⊃ (∀w1.a(w,w1,s,succ(t)) ≡ a(w,w1,s,t) ∧ true(p,w1))|)
(axiom |∀s p t.learnsw(s,p,t) = learns(s,p,t) or1 learns(s,not1 p,t)|)
;;; Now we need to be able to define a state of ignorance - or better,
;;; ignorance of a subject matter.
;;; We can say that a person knows just the value of the function foo
;;; of the state of the world at time t by writing
(decl state |world→state| constant)
(decl foo |state → ground|)
(decl knowsv |person⊗(state→ground)⊗time → proposition| constant)
(decl (x x0 x1 x2) ground)
(axiom |∀s w foo t.true1(knowsv(s,foo,t),w) ≡
(∀w1.a(w,w1,s,t) ⊃ foo(state(w1)) = foo(state(w))) ∧
(∀x.foo(x) = foo(state(w)) ⊃ ∃w1.state(w1) = x)|)
;;; It looks like we will have to assimilate knowing propositions
;;; to knowing the truth values of propositions. There should be
;;; no problem with doing this directly in EKL.
;;; Here come the wisemen axioms in the new formalism.
(proof wisemen)
(context know3ax#1:*)
(decl (wise1 wise2 wise3,ws0) person constant person)
(decl (white1 white2 white3) proposition constant proposition)
(axiom |true(white1 and1 white2 and1 white3,RW)|)
(define |ws0 = join(wise1,wise2,wise3)|)
(axiom |true1(knows(ws0,white1 or1 white2 or1 white3,0),RW)|)
(axiom|true1(knows(ws0,
knowsw(wise1,white2,0)
and1 knowsw(wise1,white3,0)
and1 knowsw(wise2,white1,0)
and1 knowsw(wise2,white3,0)
and1 knowsw(wise3,white1,0)
and1 knowsw(wise3,white2,0),0),RW)|)
(axiom |true1(
learnsw(ws0,knowsw(wise1,white1,0),0) and1
learnsw(ws0,knowsw(wise2,white2,0),0) and1
learnsw(ws0,knowsw(wise3,white3,0),0),RW)|)
(axiom |true1(
learnsw(ws0,knowsw(wise1,white1,1),1) and1
learnsw(ws0,knowsw(wise2,white2,1),1) and1
learnsw(ws0,knowsw(wise3,white3,1),1),RW)|)